Code and Notes (Week 5 Tuesday)

The goal is, for instance, to take this step of the M-machine:

Plus (Num v1) (Num v2) |->M Num (v1 + v2)

We want to place that step *in context*:

A (s ≻ Plus (Num v1) (Num v2)) |->M A (s ≻ Num (v1 + v2))

More generally, we want to show:

       e1 |->M e1'
---------------------------
A (s ≻ e1) |->M A (s ≻ e1')

The proof here, if we did it formally, would be by induction on the
stack s, which is just a list.

We set out to prove
∀s. ∀e1 e1'. e1 |->M e1'  -→  A (s ≻ e1) |->M A (s ≻ e1'),
by induction on the length of the stack s.

The base case is where the list is empty (or length 0). In that case,
∀e. A (s ≻ e) ≡ e, and our implication is trivial.

The step case is where the list has one more element than in the IH.
So, let us say our stack has the shape (f ▷ s), one more frame than s,
and our IH applies to s.

For some e1 and e1', we assume e1 |->M e1' and want to show:

A ((f ▷ s) ≻ e1) |->M A ((f ▷ s) ≻ e1')

A is defined by recursion on the stack (good!) and then by case
division on the shape of f, the topmost stack element. Our proof
does the same case division.

So, for instance, in the case where f is "Plus □ e2",

A ((f ▷ s) ≻ e1) = A (((Plus □ e2) ▷ s) ≻ e1)
  ≡ A (s ≻ Plus e1 e2)

and

A ((f ▷ s) ≻ e1') = A (((Plus □ e2) ▷ s) ≻ e1)
  ≡ A (s ≻ Plus e1' e2)

So our goal can be rewritten to:

A (s ≻ Plus e1 e2) |->M A(s ≻ Plus e1' e2)

Our IH applies to this goal shape, and tells us it is true if
we can establish this:

Plus e1 e2 |->M Plus e1' e2

We already have e1 |->M e1', and this is just the left
contextual rule for M-steps of Plus, or alternatively, the
left contextual rule for Plus in our small-step relation for
the semantics of MinHS.

Likewise, in the case where f has the shape Plus v1 □, the
definition of A gives us

A ((f ▷ s) ≻ e1) = A (((Plus v1 □) ▷ s) ≻ e1)
  ≡ A(s ≻ Plus (Num v1) e1)

(Note the detail we are insisting on, when the "hole" is at
the right operand of Plus, we assume that the left operand is
reduced to a value (v1 as opposed to Num v1)).

Again, this case of the proof boils down to an application of
one of the contextual rules from our small-step language definition.

double_hs :: Int -> Int
double_hs x = x + x

divBy5 :: Int -> Int
divBy5 x = if x < 5 then 0 else 1 + divBy5 (x - 5)

add :: Int -> Int -> Int
add x y = x + y

data MinHS =
  Num Int
  | Lit Bool
  | If MinHS MinHS MinHS
  | Apply MinHS MinHS
  | Recfun Type Type (MinHS -> MinHS -> MinHS)
  | Plus MinHS MinHS
  | Minus MinHS MinHS
  | Eq MinHS MinHS
  | Times MinHS MinHS
  | LessThan MinHS MinHS
  | Tag String
  | TypeTag Type

data Type = BoolTy | IntTy | FunTy Type Type
  deriving (Eq,Show)
  -- tells Haskell to automatically define a pretty-printer
  -- and equality comparisons for our type

data Value = Bool_Val Bool | Int_Val Int
    | Fun_Val (MinHS -> MinHS -> MinHS)

double_minhs :: MinHS
double_minhs = Recfun IntTy IntTy (\f x -> Plus x x)

divBy5_minhs :: MinHS
divBy5_minhs = Recfun IntTy IntTy (\f x -> If (LessThan x (Num 5))
   (Num 0) (Plus (Num 1) (Apply f (Minus x (Num 5)))))

add_minhs :: MinHS
add_minhs = Recfun IntTy (FunTy IntTy IntTy) (\f x ->
    Recfun IntTy IntTy (\f y -> Plus x y))

-- to print (\f x -> Plus x x), we will invent some
-- special values "f" and "x" and pass them to the function

printer :: MinHS -> String
printer minhs = case minhs of
  Num n -> show n
  Lit b -> show b
  Plus x y -> concat ["(", printer x, " + ", printer y, ")"]
  Minus x y -> concat ["(", printer x, " - ", printer y, ")"]
  Eq x y -> concat ["(", printer x, " == ", printer y, ")"]
  LessThan x y -> concat ["(", printer x, " < ", printer y, ")"]
  Apply x y -> concat ["(", printer x, " ", printer y, ")"]
  If c x y -> concat ["(if ", printer c, " then ", printer x,
        " else ", printer y, ")"]
  Recfun t1 t2 f ->
    let f_nm = "f" in
    let x_nm = "x" in
    concat ["(recfun ", f_nm, " :: (", show t1, " -> ", show t2,
        ") ", x_nm, " = ", printer (f (Tag f_nm) (Tag x_nm))]
  Tag nm -> nm
  TypeTag ty -> ("(TypeTag " ++ show ty ++ ")")
  _ -> error ("MinHS pretty-printer: unimplemented")

-- Skipped for now: fix the pretty-printer to not always use
-- the same name "x". It is pretty broken at the moment.

check :: MinHS -> Type -> Bool
check x ty = (if type_checker x == ty
    then True
    else error ("check: types disagree for " ++
        show (printer x, ty, type_checker x)))

type_checker :: MinHS -> Type
type_checker (Tag nm) = error ("type_checker: Tag should not appear")
type_checker (TypeTag ty) = ty
type_checker (Recfun t1 t2 f) =
    if check (f (TypeTag (FunTy t1 t2)) (TypeTag t1)) t2
    then FunTy t1 t2
    else error ("Recfun: invalid types")
type_checker (Apply f x) = case type_checker f of
    FunTy t1 t2 -> if check x t1 then t2 else (error "Apply: types")
    t -> error ("type_checker: application of " ++ show t)
type_checker (Plus x y) = if check x IntTy && check y IntTy
    then IntTy else error ("Plus: invalid types")
type_checker (Minus x y) = if check x IntTy && check y IntTy
    then IntTy else error ("Minus: invalid types")
type_checker (Eq x y) = if check x IntTy && check y IntTy then BoolTy
    else error ("Plus: invalid types")
type_checker (LessThan x y) = if check x IntTy && check y IntTy
    then BoolTy else error ("Plus: invalid types")
type_checker (If c x y) = if check c BoolTy then
        let t = type_checker x in
        if check y t then t else error ("If: invalid types")
    else error ("If: condition not a boolean")
type_checker (Num n) = IntTy
type_checker (Lit b) = BoolTy
type_checker x = error ("type_checker: unimplemented: " ++ printer x)



-- To type-check Recfun t1 t2 (\f x -> body), we will need
-- (in type-checking the body) just that x has type t2 and
-- f has type (FunTy t1 t2). So we replace f with TypeTag ...


eval :: MinHS -> MinHS
eval e = case e of
  Num _ -> e
  Lit _ -> e
  Recfun _ _ _ -> e
  Apply f x ->
    let f2 = eval f in
    let x2 = eval x in
    case f2 of
      Recfun _ _ body_fn -> eval (body_fn f2 x2)
      exp -> error ("eval: type-incorrect apply of " ++ printer exp)
  _ -> error ("eval: unimplemented: " ++ printer e)


data MinHS_Frame =
  Plus_Frame_1 () MinHS
  | Plus_Frame_2 Value ()
  | If_Frame () MinHS MinHS
  | Apply_Frame_2 () MinHS
  | Apply_Frame_1 Value ()

eval_frame :: MinHS -> [MinHS_Frame] -> Value
eval_frame (Plus e1 e2) stack =
    eval_frame e1 ([Plus_Frame_1 () e2] ++ stack)
eval_frame (Num n) stack = push_val_frame (Int_Val n) stack

push_val_frame :: Value -> [MinHS_Frame] -> Value
push_val_frame v [] = v
push_val_frame v (Plus_Frame_1 () e : stack) =
    eval_frame e (Plus_Frame_2 v () : stack)
push_val_frame (Int_Val i1) (Plus_Frame_2 (Int_Val i2) () : stack) =
    push_val_frame (Int_Val (i1 + i2)) stack


print_val :: Value -> String
print_val (Int_Val i) = show i
print_val (Bool_Val b) = show b